function tribonacci(n: nat) : nat
{
	if n == 0 then 0
	else if n == 1 then 0
	else if n == 2 then 1
	else tribonacci(n - 1) + tribonacci(n - 2) + tribonacci(n - 3)
}

method compute_tribonacci(n: nat) returns (f: nat)
ensures f == tribonacci(n)
{
	if n <= 1
	{
		return 0;
	}
	else if n == 2 {
		return 1;
	}

	var t0 := 0;
	var t1 := 0;
	var t2 := 1;

	var i := 3;
	while i < n
	invariant 3 <= i <= n
	invariant t0 == tribonacci(i - 3)
	invariant t1 == tribonacci(i - 2)
	invariant t2 == tribonacci(i - 1)
	{
		t0, t1, t2 := t1, t2, t0 + t1 + t2;
		i := i + 1;
	}

	return t0 + t1 + t2;
}

function count_zeros_from(xs: array<int>, from_index: int) : int
reads xs
requires 0 <= from_index <= xs.Length
decreases xs.Length - from_index
{
	if from_index == xs.Length then 0
	else (if xs[from_index] == 0 then 1 else 0) + count_zeros_from(xs, from_index + 1)
}

method imperative_count_zeros(xs: array<int>) returns (count: int)
ensures count == count_zeros_from(xs, 0)
{
	count := 0;
	var i := 0;
	while i < xs.Length
	invariant 0 <= i <= xs.Length
	invariant count_zeros_from(xs, 0) == count_zeros_from(xs, i) + count
	{
		count := count + (if xs[i] == 0 then 1 else 0);
		i := i + 1;
	}
	return count;
}